
(**************************************************************************)
(*       ___                                                              *)
(*      ||M||                                                             *)
(*      ||A||       A project by Andrea Asperti                           *)
(*      ||T||                                                             *)
(*      ||I||       Developers:                                           *)
(*      ||T||         The HELM team.                                      *)
(*      ||A||         http://helm.cs.unibo.it                             *)
(*      \   /                                                             *)
(*       \ /        This file is distributed under the terms of the       *)
(*        v         GNU General Public License Version 2                  *)
(*                                                                        *)
(**************************************************************************)

include "arithmetics/nat.ma".
include "basics/bool.ma".
include "basics/lists/list.ma".
include "basics/logic.ma".

inductive integer : Type[0] ≝
  int : bool → nat → integer. (* -0, +0 ?*)
notation "+x" with precedence 80 for @{int true $x}.
notation "-x" with precedence 80 for @{int false $x}.

inductive struct_one : Type[0]≝
  atom : integer→ struct_one
| unit : struct_one.

inductive operator : Type[0] ≝
  par : operator
| copar : operator
| seq : operator
.  

inductive struct : Type[0] ≝
   s1 : operator → list struct → struct
|  s2 : struct_one → struct.


(* equality on operators *) 
definition eqb_op ≝ λo1,o2.match o1 with[
  par ⇒ match o2 with [ par ⇒ true | _ ⇒ false]
  | copar ⇒ match o2 with [copar ⇒ true | _ ⇒ false ]
  | seq ⇒ match o2 with [seq ⇒ true | _ ⇒ false]].

lemma eq_op : ∀o1,o2.(eqb_op o1 o2=true) ↔ (o1=o2) .
#O1 #O2 elim O1 elim O2 %
normalize //
#A destruct qed.

lemma eq_op1 : ∀o1,o2.(eqb_op o1 o2=true) → o1=o2.
#O1 #O2 lapply (eq_op O1 O2)
*

 /2/ qed.

lemma eq_op2 : ∀o1,o2.o1=o2→ (eqb_op o1 o2=true).
#O1 #O2 lapply (eq_op O1 O2)
* /2/ qed.
     

(* notation for atoms and unit. For example: «atom n»  with n ∈ ℕ , «unit» *)
notation "«x»" with precedence 70 
for @{s2 ($x)}.
(* usefule abbreviations for atoms*)
notation "𝕒" with precedence 80 for @{(«atom +1»)}.
notation "𝕓" with precedence 80 for @{(«atom +2»)}.
notation "𝕔" with precedence 80 for @{(«atom +3»)}.

(*notation for structures, x is a list of struct *)
notation "〚x〛" with precedence 45
for @{s1 par $x}.

notation "❬x❭" with precedence 45
for @{s1 seq $x}.

notation "❨x❩" with precedence 45
for @{s1 copar $x}.
  
(* Given a list of structures l and an operator op
   create_struct_r replaces every occurrence of 
        s1 op sub_l
   in l with
        sub_l                                           *) 
let rec create_struct_r (l:list struct) (op:operator) on l ≝
match l with [
  nil ⇒ [ ]
| cons h tl ⇒ match h with [
          s1 sub_op sub_l ⇒ (if (eqb_op sub_op op) then sub_l else h::[])@(create_struct_r tl op)
        | _ ⇒ (h::[])@(create_struct_r tl op)]
].

(* Given a  list l = (S1 o1 l1)::...::(Si oi li)::...::(Sn on ln) of structures 
    where if (s1 ox lx) ∈ li → ox≠oi 
    and an operator o
   create_struct yields a structure 
   s1 o  (S1' o1' l1')::...::(Si' oi' li')::...::(Sm' om' lm')
   where no one among o1',..., om' can be equal to the given o.    *)
definition create_struct ≝λl.λo.s1 o (create_struct_r l o).
                                
(* c_s_nil stands for creates_structure_nil 
   QUESTION: 
   does this structure correspond to any structure of BV, as defined
   in the standard literature?
   This is not necessarily be a problem, but it is good to remark
   this anomaly, if it is an anomaly. *)
(*It is, maybe this equality can solve that? 
    definition s1_nil_to_unit ≝∀op.s1 op [ ] = s2 unit.*)
    lemma c_s_nil: ∀o.create_struct [] o =s1 o [].
      #O normalize // qed.

(* If we use create_struct to 
   create a structure s1, whose main operator is o applied to the list of structures ls,
   then, in fact, we build a structure s1 o l, where l is not necessarily ls, but a shorter list. 
   QUESTION:
   Is it exactly what we want?
   Example:
   Isn't it true that
     create_struct s1 (s1 par [a , b]::(s1 seq [c , d]::(s1 par [e , f]) par 
        = s1 par [a , b]::(s1 seq [c , d])::[e , f]  ?
   In case of positive answer, is it what we want, or do we know how to manage
   this interleaving of lists of structures with structures?
*) (* Non ho capito la domanda.*)
lemma c_s_exists : ∀ls:list struct.∀o:operator.∃l:list struct.(create_struct ls o) = s1 o l.
#L #O  % // qed.



(* Couldn't the following statement:
lemma structures_are_stratified:
∀l, left_list, mid_list, right_list: list struct.
  create_struct l o1 = s1 o1 (left_list::mid_list::right_list).
    →  ∃ ol. ∃ sll. left_list = s1 ol sll
      →  ∃ om. ∃ slm. mid_list  = s1 om slm 
        →  ∃ or. ∃ slr. right_list = s1 or slr → ¬(ol=om) ∧ ¬(ol=or) ∧ ¬(om=or) .
hold in place of c_s_head1 here below?
*)(* Idem, non ho capito *)
lemma c_s_head1 : ∀l,sub_l:list struct.∀s:struct.∀o1,o2.
  s=s1 o1 sub_l → ¬(o1=o2) → ∃l2.create_struct (s::l) o2 = s1 o2 (s::l2).
      #LS #SUBL #ST #O1 #O2 
      #HIP1
      #HIP2
      % 
      [ @(create_struct_r LS O2) |
      >HIP1
      normalize
      lapply HIP2
      elim O1 elim O2
      normalize //
      * #H destruct
      lapply (H ?)  //
      * qed.




lemma c_s_head2 : ∀l:list struct.∀s:struct.∀t:struct_one.∀o.
        s=s2 t → ∃l2.create_struct (s::l) o = s1 o (s::l2).
        #L #S #T #O
        #HIP1
        %
        [ @(create_struct_r L O) |
        >HIP1  
        normalize //] qed.

lemma c_s_head3 : ∀l,subl:list struct.∀s:struct.∀o.
            s=s1 o subl → ∃l2.create_struct (s::l) o = s1 o (subl@(l2)).
            
            #L #SUBL #S #O
            #HIP1
            %
            [ @(create_struct_r L O) |
            >HIP1 normalize
            elim O
            normalize //] qed.
            

(* useful definitions and lemma for the next theorem*)
definition neq_op_s ≝λo.λs. match s with [ s1 op l ⇒ op≠o | _ ⇒ True].

lemma append_cons_s : ∀A.∀a:A.∀l. a::l=[a]@l.
#A #a #L // qed.

lemma All_append_l : ∀A,P,l1,l2.
  All A P (l1 @ l2) → All A P l1 ∧ All A P l2.
  #A #P #L1 #L2
elim L1
normalize [  /2/
] #H1 #H2 #H3 *
 #H4 #H5  %[ % [ @H4 | lapply (H3 H5) * #H6 #H7 @H6] |
 lapply (H3 H5) *#H9 #H10 @H10 qed.    

lemma All_append_r : ∀A,P,l1,l2.
 All A P l1 ∧ All A P l2 →   All A P (l1 @ l2).
    #A #P #L1 #L2 *
    elim L1 //
    #H #TL
    #IND  #HIP1 #HIP2

normalize % normalize in HIP1; lapply HIP1 * #H12 #H13 /2/ qed.    
definition is_ass_norm_1_degree ≝λs.match s with [
          s1 op l ⇒ All ? (neq_op_s op) l
        | s2 t ⇒ True].

theorem prova : 
  ∀o.∀l. (All ? (is_ass_norm_1_degree) l) →   is_ass_norm_1_degree (create_struct l o).
#O
elim O
  
  #L
  elim L (*Induco su L*)
    [1,3,5: // (*Se è vuota è banale*) 
    |2,4,6: 
      #H #TL #IND
      (*Forse mi serve parlare di append più che di cons*)
      lapply (append_cons_s ? H  TL) #APPEQ >APPEQ -APPEQ 
      (*Ora spezzo tutte le ipotesi*)
      #HIP lapply (All_append_l ? ? ? ? HIP) * -HIP #HIP1 #HIP2 
      lapply (IND HIP2) -IND #IND 
      lapply HIP1 -HIP1
      elim H (*Induco sulla testa della lista così posso ridurre*)
        [1,3,5:
          #O2 #SUBL #HIP1
          normalize
          lapply HIP1 -HIP1
          (*Ora induco sul secondo operatore:fa esplodere abbastanza la dimostrazione*)
          elim O2 #HIP1           
          normalize
          (*Ora prendo le dimostrazioni con gli operatori uguali*)
          [1,5,9:           
            @All_append_r %
            [2,4,6:
              normalize in IND;
              //
            |1,3,5:
              normalize in HIP1; 
              lapply HIP1 -HIP1 * #HIP1 #T //
            ]
            (*Ora prendo le dimostrazioni con operatori diversi*)
            |2,3,4,6,7,8:  %
            [1,3,5,7,9,11: % #ABS destruct |2,4,6,8,10,12: // ]
          ] |2,4,6: #T #HIP1 @All_append_r % // 
      ]
   ]
qed.

  let rec is_ass_norm s ≝ match s with [
        s1 op l ⇒ (All ? (neq_op_s op) l) ∧ (All ? is_ass_norm l)
      | s2 t ⇒ True].
      
      
      
theorem prova2: ∀o.∀l.All ? is_ass_norm l → is_ass_norm (create_struct l o).
(* following the previous theorem *)
#O elim O
#L elim L 
[1,3,5:  normalize * %  //  |2,4,6: #H #TL #IND
lapply (append_cons_s ? H  TL) #APPEQ >APPEQ -APPEQ 
#HIP lapply (All_append_l ? ? ? ? HIP) * -HIP #HIP1 #HIP2 
lapply (IND HIP2) -IND #IND lapply HIP1 -HIP1
elim H 
[1,3,5: #O2 #SUBL #HIP1 normalize
lapply HIP1 -HIP1
elim O2 #HIP1 
normalize
[1,5,9: %
@All_append_r %
[1,3,5,7,9,11: lapply HIP1 normalize * -HIP1 * //
|2,4,6,8,10,12: lapply IND normalize * //
]
|2,3,4,6,7,8:% %  (* Qui le cose si moltiplicano più del dovuto, ma per ora mi accontento di
        saperle chiudere*)
[1,5,9,13,17,21: % #ABS   destruct
|2,4,6,8,10,12,14,16,18,20,22,24: lapply IND normalize * //
|3,7,11,15,19,23: lapply HIP1 normalize * //
]
] 
|2,4,6:
#T normalize * #T #T % 
[1,3,5: %
[1,3,5: //
|2,4,6: lapply IND normalize * //
]
|2,4,6: %
[1,3,5: //
|2,4,6: lapply IND normalize * // qed.

definition is_s_base ≝λs.match s with [s2 t ⇒ True | _ ⇒ False ].

lemma perprova3: ∀s.is_s_base s → is_ass_norm s.
#S elim S
[ #O #L normalize * |
#T normalize * //] qed.


theorem prova3: ∀o.∀l.All ? is_s_base l → is_ass_norm (create_struct l o).
#O #L #HIP
lapply (All_mp ? (is_s_base) (is_ass_norm) perprova3 L HIP) -HIP @prova2 qed.


(*notation "??" with precedence 80 for @{creatre_struct ??}*)

(* Given a struct s and a list of nats g find the wanted sub struct in s following 
  the elements of g. If the sub struct doesn't exist returns otherw.

*)
let rec nth_s (s:struct) (g:list nat) (otherw: struct) on g ≝
match s with [
  s1 op l ⇒ match g with [
      cons h tl ⇒ nth_s (nth h ? l otherw) tl otherw
    | nil ⇒ s
  ]
| s2 t ⇒ otherw  (* Or t, who knows?*)
].

definition is_not_unit ≝λs.match s with [s2 t ⇒ match t with [  unit ⇒ false | _ ⇒ true ] | _ ⇒ true ].
definition filter_unit_base ≝ filter struct is_not_unit.

(* Remove ALL units from struct s*)
let rec filter_unit s≝  match s with [
    s1 op l ⇒ s1 op (filter_unit_base (map ? ? filter_unit l))
  | s2 t ⇒ s2 t].

(*lemma dadimostrare:∀l.∀s.nth_s (filter_unit s) l 𝕒≠«unit».*)





(*lemma funziona : (filter_unit (s1 copar [(s1 par [«unit»;𝕒;«unit»;𝕓]);«unit»])) = ?. normalize*)

  
(* lemma funziona: neg (❨[〚[𝕒;𝕓]〛;«unit»;«atom -1»]❩)=?. normalize *)
  

lemma eq_f_map : ∀A:Type[0].∀f,g:A→ A.∀l.map A A f (map A A g l) = map A A (f∘g) l.
#A #F #G #L
elim L
//
#H #TL #IND
normalize
>IND // qed.

definition neg_op ≝ λo. match o with [
  par   ⇒ copar
| copar ⇒ par
| seq   ⇒ seq ].

(* l'ho riscirtta leggeremente *)
let rec neg s ≝
  match s with [
      s1 op l ⇒ s1 (neg_op op) (map ? ? neg l) 
    | s2 t ⇒ match t with [
               atom i ⇒ match i with [ int b n ⇒ s2 (atom (int (¬b) n)) ]
             | unit  ⇒ s2 unit  
    ]
  ].
  
  
  
let rec size_struct b ≝
  match b with [
      s2  t ⇒ 0
   |  s1 op l ⇒  \fold[plus,1]_{i∈l} (size_struct i)].
   
   
lemma negbase : ∀t:struct_one.neg (neg (s2 t) )= (s2 t).
#T elim T [ #I elim I #B #X elim B normalize // | // qed.
     
     
theorem negIdem : ∀s.neg (neg s) = s.
  #s
  (* Per induzione sulla dimensione dela struttura*) 
  cut (∃n. size_struct s =n)
  
  [% {(size_struct s)} //] (*La dimensione esiste sempre*)
  * #n lapply s -s @(nat_elim1 n) (*Induzione sulla dimensione*)
  -n #m #H #s cases s
  [  (* Se s è una struttura con lista *)
    #O #l 
     cases l (*Induzione sulla lista interna *)
      [ (*Lista vuota*)
        #H1  elim O normalize  //
       | (*Lista con almeno un elemento *)
         #st #l1 #H1 normalize
          @eq_f2 (*Spezzo la lista*)
          [ elim O //] (*Gli operatori non sono rilevanti*)
          @eq_f2
           [ (*Head*)
              @(H … (refl  …)) (*La dimenione della head è minore del totale?*)
              <H1 >(plus_n_O (size_struct st)) in ⊢ (?%?); whd
              >(plus_n_Sm (size_struct st) 0) in ⊢ (?%?); @monotonic_le_plus_r
              elim l1 (*Induzione sulla coda*) // #a #tl normalize /2/ 
           | (*Tail*)
              normalize in H1; lapply(sym_eq nat …H1)  >commutative_plus -H1 #H1 lapply (eq_plus_to_le … H1)-H1 
              elim l1 (*Induzione sulla coda*)
              // (*Coda vuota*)
              #b2 #l2 #Hind normalize #H1 @eq_f2
              [ (*Spezzo la lista, Head*)
                @(H … (refl …)) @(lt_to_le_to_lt … H1) >(plus_n_O (size_struct b2)) in ⊢ (?%?); whd
               >(plus_n_Sm (size_struct b2) 0) in ⊢ (?%?); @monotonic_le_plus_r
               elim l2 // #a #tl normalize /2/
               |
              @Hind /2/
             ] 
        ]
    ] | #T // (*Caso base*)
 ] .
 
 
 
 
 



(* Useless?
definition leb_op ≝λo1,o2:operator. match o1 with [
      par ⇒ true
    | copar ⇒ match o2 with [ par ⇒ false | _ ⇒ true]
    | seq ⇒ match o2 with [ seq ⇒ true | _ ⇒ false ]].
    
    
definition leb_int ≝λi1,i2:integer.match i1 with [
      int b1 n1 ⇒ match i2 with [
            int b2 n2 ⇒ match (eqb n1 n2) with [
                  true ⇒ b2
                | false ⇒ leb n1 n2
                  ] 
                  
            ]
       ].
definition leb_sone ≝λt1,t2:struct_one. match t1 with [
      atom i1 ⇒ match t2 with [
                atom i2 ⇒ leb_int i1 i2
              | unit ⇒ false
              ]
    | unit ⇒ true].
    
    
let rec zipWith (A,B,C:Type[0]) (f:(A→B→C)) (l1:(list A)) (l2:(list B)) on l1 ≝
        match l1 with [
            nil ⇒  []
          | cons ha tla ⇒ match l2 with [
                nil ⇒  []
              | cons hb tlb ⇒ (f ha hb)::(zipWith A B C f tla tlb)
              ]
        ].
        
        
  
let rec leb_s sx sy ≝ match sx with [
    s1 opx lx ⇒ match sy with [
          s1 opy ly ⇒ match (eqb (|lx|) (|ly|)) with [
                true ⇒ foldr ? ? (andb) true (zipWith struct struct bool (leb_s) lx ly)
              | false ⇒ leb (|lx|) (|ly|)
          ]
  | s2 t ⇒ false
  ] | s2 tx ⇒ match sy with [
              s1 opy ly ⇒ true
            | s2 ty ⇒ leb_sone tx ty
            ]
    ].
    





definition term ≝ 〚([«unit»;〚([𝕔])〛])〛.

definition term2 ≝ 〚([«unit»;〚([𝕓])〛])〛.


let rec splitr_4_msort (A:Type[0]) (l:list A) n left right on l≝ match l with [
      nil ⇒ (mk_Prod ? ? left right)
    | cons h tl ⇒ match n with [
            O ⇒ splitr_4_msort A tl 1 (left@[h]) right
          | _ ⇒ splitr_4_msort A tl 0 left (right@[h]) 
      ]
 ]
.

definition split_4_msort ≝λl.splitr_4_msort struct l 0 [ ] [ ].



let rec merge (A:Type[0]) (l1:list A) (l2:list A) (leq:A→ A→ bool) on l1: list A≝
  match l1 with [
      nil ⇒ l2
    | cons h1 tl1 ⇒ match l2 with [
          nil ⇒ l1
        | cons h2 tl2 ⇒ match (leq h1 h2) with [
                true ⇒  h1::(merge ? tl1 l2 leq)
              | false ⇒ (filter ? (λz.¬(leq h1 z)) l2)@(h1::(merge ? tl1 (filter ? (leq h1)  l2) leq ))
              ]
      ]
  ].
  
definition l1 ≝ [«unit»;𝕒;𝕒;𝕓].
definition l2 ≝[𝕒;𝕒;𝕒;𝕓;𝕔].
  
  
  
let rec msort_r (l:list struct) n on n ≝
match n with [O ⇒ nil struct | S  m ⇒ 
    let x ≝ split_4_msort l in 
        let l1 ≝ msort_r (\fst x) m in 
        let l2 ≝ msort_r (\snd x) m in 
        merge ? l1 l2 leb_s
].

definition msort ≝λl.msort_r l 10 (*Con 50 già impazzisce!*).
*)

